Inference at * 1 1 
Iof proof for Lemma member-exists:



1. T : Type
2. x:T. (x  [])
  ([] = []) 

latex

 by ((ExRepD) 
CollapseTHEN (Obvious)) 

latex

C.

Definitions	{T}, x:A. B(x), P  Q, P & Q, P  Q, P  Q, x:AB(x), False, , t  T, [], x:A. B(x), x:A  B(x), A, s = t, type List, , {x:A| B(x)} , , A  B, a < b, ||as||, Y, x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), n+m, l[i], hd(l), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), i z j, b, i <z j, if a<b then c else d, n - m, tl(l), Type, (x  l)
Lemmas	nil member, not wf, false wf